Serveur d'exploration sur la recherche en informatique en Lorraine

Attention, ce site est en cours de développement !
Attention, site généré par des moyens informatiques à partir de corpus bruts.
Les informations ne sont donc pas validées.

A new combination procedure for the word problem that generalizes fusion decidability results in modal logics

Identifieur interne : 005627 ( Main/Exploration ); précédent : 005626; suivant : 005628

A new combination procedure for the word problem that generalizes fusion decidability results in modal logics

Auteurs : Franz Baader [Allemagne] ; Silvio Ghilardi [Italie] ; Cesare Tinelli [États-Unis]

Source :

RBID : Pascal:06-0527634

Descripteurs français

English descriptors

Abstract

Previous results for combining decision procedures for the word problem in the non-disjoint case do not apply to equational theories induced by modal logics-which are not disjoint for sharing the theory of Boolean algebras. Conversely, decidability results for the fusion of modal logics are strongly tailored towards the special theories at hand, and thus do not generalize to other types of equational theories. In this paper, we present a new approach for combining decision procedures for the word problem in the non-disjoint case that applies to equational theories induced by modal logics, but is not restricted to them. The known fusion decidability results for modal logics are instances of our approach. However, even for equational theories induced by modal logics our results are more general since they are not restricted to so-called normal modal logics.


Affiliations:


Links toward previous steps (curation, corpus...)


Le document en format XML

<record>
<TEI>
<teiHeader>
<fileDesc>
<titleStmt>
<title xml:lang="en" level="a">A new combination procedure for the word problem that generalizes fusion decidability results in modal logics</title>
<author>
<name sortKey="Baader, Franz" sort="Baader, Franz" uniqKey="Baader F" first="Franz" last="Baader">Franz Baader</name>
<affiliation wicri:level="1">
<inist:fA14 i1="01">
<s1>Institut fur Theoretische Informatik, TU Dresden</s1>
<s3>DEU</s3>
<sZ>1 aut.</sZ>
</inist:fA14>
<country>Allemagne</country>
<wicri:noRegion>TU Dresden</wicri:noRegion>
<wicri:noRegion>Institut fur Theoretische Informatik, TU Dresden</wicri:noRegion>
</affiliation>
</author>
<author>
<name sortKey="Ghilardi, Silvio" sort="Ghilardi, Silvio" uniqKey="Ghilardi S" first="Silvio" last="Ghilardi">Silvio Ghilardi</name>
<affiliation wicri:level="1">
<inist:fA14 i1="02">
<s1>Dipartimen to di Scienze dell'Informazione, Università degli Studi di Milano</s1>
<s3>ITA</s3>
<sZ>2 aut.</sZ>
</inist:fA14>
<country>Italie</country>
<wicri:noRegion>Dipartimen to di Scienze dell'Informazione, Università degli Studi di Milano</wicri:noRegion>
</affiliation>
</author>
<author>
<name sortKey="Tinelli, Cesare" sort="Tinelli, Cesare" uniqKey="Tinelli C" first="Cesare" last="Tinelli">Cesare Tinelli</name>
<affiliation wicri:level="4">
<inist:fA14 i1="03">
<s1>Department of Computer Science, The University of Iowa</s1>
<s3>USA</s3>
<sZ>3 aut.</sZ>
</inist:fA14>
<country>États-Unis</country>
<placeName>
<settlement type="city">Iowa City</settlement>
<region type="state">Iowa</region>
</placeName>
<orgName type="university">Université de l'Iowa</orgName>
</affiliation>
</author>
</titleStmt>
<publicationStmt>
<idno type="wicri:source">INIST</idno>
<idno type="inist">06-0527634</idno>
<date when="2006">2006</date>
<idno type="stanalyst">PASCAL 06-0527634 INIST</idno>
<idno type="RBID">Pascal:06-0527634</idno>
<idno type="wicri:Area/PascalFrancis/Corpus">000416</idno>
<idno type="wicri:Area/PascalFrancis/Curation">000617</idno>
<idno type="wicri:Area/PascalFrancis/Checkpoint">000417</idno>
<idno type="wicri:explorRef" wicri:stream="PascalFrancis" wicri:step="Checkpoint">000417</idno>
<idno type="wicri:doubleKey">0890-5401:2006:Baader F:a:new:combination</idno>
<idno type="wicri:Area/Main/Merge">005822</idno>
<idno type="wicri:Area/Main/Curation">005627</idno>
<idno type="wicri:Area/Main/Exploration">005627</idno>
</publicationStmt>
<sourceDesc>
<biblStruct>
<analytic>
<title xml:lang="en" level="a">A new combination procedure for the word problem that generalizes fusion decidability results in modal logics</title>
<author>
<name sortKey="Baader, Franz" sort="Baader, Franz" uniqKey="Baader F" first="Franz" last="Baader">Franz Baader</name>
<affiliation wicri:level="1">
<inist:fA14 i1="01">
<s1>Institut fur Theoretische Informatik, TU Dresden</s1>
<s3>DEU</s3>
<sZ>1 aut.</sZ>
</inist:fA14>
<country>Allemagne</country>
<wicri:noRegion>TU Dresden</wicri:noRegion>
<wicri:noRegion>Institut fur Theoretische Informatik, TU Dresden</wicri:noRegion>
</affiliation>
</author>
<author>
<name sortKey="Ghilardi, Silvio" sort="Ghilardi, Silvio" uniqKey="Ghilardi S" first="Silvio" last="Ghilardi">Silvio Ghilardi</name>
<affiliation wicri:level="1">
<inist:fA14 i1="02">
<s1>Dipartimen to di Scienze dell'Informazione, Università degli Studi di Milano</s1>
<s3>ITA</s3>
<sZ>2 aut.</sZ>
</inist:fA14>
<country>Italie</country>
<wicri:noRegion>Dipartimen to di Scienze dell'Informazione, Università degli Studi di Milano</wicri:noRegion>
</affiliation>
</author>
<author>
<name sortKey="Tinelli, Cesare" sort="Tinelli, Cesare" uniqKey="Tinelli C" first="Cesare" last="Tinelli">Cesare Tinelli</name>
<affiliation wicri:level="4">
<inist:fA14 i1="03">
<s1>Department of Computer Science, The University of Iowa</s1>
<s3>USA</s3>
<sZ>3 aut.</sZ>
</inist:fA14>
<country>États-Unis</country>
<placeName>
<settlement type="city">Iowa City</settlement>
<region type="state">Iowa</region>
</placeName>
<orgName type="university">Université de l'Iowa</orgName>
</affiliation>
</author>
</analytic>
<series>
<title level="j" type="main">Information and computation : (Print)</title>
<title level="j" type="abbreviated">Inf. comput. : (Print)</title>
<idno type="ISSN">0890-5401</idno>
<imprint>
<date when="2006">2006</date>
</imprint>
</series>
</biblStruct>
</sourceDesc>
<seriesStmt>
<title level="j" type="main">Information and computation : (Print)</title>
<title level="j" type="abbreviated">Inf. comput. : (Print)</title>
<idno type="ISSN">0890-5401</idno>
</seriesStmt>
</fileDesc>
<profileDesc>
<textClass>
<keywords scheme="KwdEn" xml:lang="en">
<term>Boolean algebra</term>
<term>Computer theory</term>
<term>Decidability</term>
<term>Decision</term>
<term>Equational theory</term>
<term>Modal logic</term>
<term>Sharing</term>
<term>Type theory</term>
<term>Word</term>
</keywords>
<keywords scheme="Pascal" xml:lang="fr">
<term>Mot</term>
<term>Décidabilité</term>
<term>Logique modale</term>
<term>Décision</term>
<term>Théorie équationnelle</term>
<term>Partage</term>
<term>Algèbre Boole</term>
<term>Théorie type</term>
<term>Informatique théorique</term>
<term>Procédure décision</term>
<term>Problème mot</term>
<term>03B45</term>
<term>06Exx</term>
<term>03B15</term>
</keywords>
<keywords scheme="Wicri" type="topic" xml:lang="fr">
<term>Décision</term>
</keywords>
</textClass>
</profileDesc>
</teiHeader>
<front>
<div type="abstract" xml:lang="en">Previous results for combining decision procedures for the word problem in the non-disjoint case do not apply to equational theories induced by modal logics-which are not disjoint for sharing the theory of Boolean algebras. Conversely, decidability results for the fusion of modal logics are strongly tailored towards the special theories at hand, and thus do not generalize to other types of equational theories. In this paper, we present a new approach for combining decision procedures for the word problem in the non-disjoint case that applies to equational theories induced by modal logics, but is not restricted to them. The known fusion decidability results for modal logics are instances of our approach. However, even for equational theories induced by modal logics our results are more general since they are not restricted to so-called normal modal logics.</div>
</front>
</TEI>
<affiliations>
<list>
<country>
<li>Allemagne</li>
<li>Italie</li>
<li>États-Unis</li>
</country>
<region>
<li>Iowa</li>
</region>
<settlement>
<li>Iowa City</li>
</settlement>
<orgName>
<li>Université de l'Iowa</li>
</orgName>
</list>
<tree>
<country name="Allemagne">
<noRegion>
<name sortKey="Baader, Franz" sort="Baader, Franz" uniqKey="Baader F" first="Franz" last="Baader">Franz Baader</name>
</noRegion>
</country>
<country name="Italie">
<noRegion>
<name sortKey="Ghilardi, Silvio" sort="Ghilardi, Silvio" uniqKey="Ghilardi S" first="Silvio" last="Ghilardi">Silvio Ghilardi</name>
</noRegion>
</country>
<country name="États-Unis">
<region name="Iowa">
<name sortKey="Tinelli, Cesare" sort="Tinelli, Cesare" uniqKey="Tinelli C" first="Cesare" last="Tinelli">Cesare Tinelli</name>
</region>
</country>
</tree>
</affiliations>
</record>

Pour manipuler ce document sous Unix (Dilib)

EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 005627 | SxmlIndent | more

Ou

HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 005627 | SxmlIndent | more

Pour mettre un lien sur cette page dans le réseau Wicri

{{Explor lien
   |wiki=    Wicri/Lorraine
   |area=    InforLorV4
   |flux=    Main
   |étape=   Exploration
   |type=    RBID
   |clé=     Pascal:06-0527634
   |texte=   A new combination procedure for the word problem that generalizes fusion decidability results in modal logics
}}

Wicri

This area was generated with Dilib version V0.6.33.
Data generation: Mon Jun 10 21:56:28 2019. Site generation: Fri Feb 25 15:29:27 2022